ds:x:Id fp Type, da:k:Knd fp Type, A, B:ecl-trans-tuple{i:l}(ds;da), f:(()()),
g:(), L, L1, l:event-info(ds;da) List.
L = (L1 @ l)
 (L':event-info(ds;da) List. L'  L  (L1  L'  ecl-trans-h(A)(0,ecl-trans-state(A;L'))))
 ecl-trans-state(combine-ecl-tuples(A;B;f;g);L)
 =
 <ecl-trans-state(A;L),ecl-trans-state(B;l)>
  ecl-trans-type(combine-ecl-tuples(A;B;f;g)) 

latex

Definitions

t  T, x:A. B(x), let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), ecl-trans-type(A), combine-ecl-tuples(A;B;f;g), ecl-trans-tuple{i:l}(ds;da), ecl-trans-state(v;L), event-info(ds;da), S  T, AB, P  Q, False, A, , Prop, ecl-trans-h(v), b, l1  l2, P  Q, as @ bs, {T}, x. t(x), , Knd, a:A fp B(a), Id, ecl-trans-state-from(v;z;L), ecl-trans-init(v), , Unit, Valtype(da;k), Top, f(x), x  dom(f), f(x)?z, State(ds), tl(l), i<j, b, ij, nth_tl(n;as), hd(l), l[i], ||as||, (x  l), list_accum(x,a.f(x;a);y;l), i=j, NatDeq, atom-deq-aux, x=yAtom, AtomDeq, IdDeq, IdLnkDeq, prod-deq(A;B;a;b), 2of(t), p  q, proddeq(a;b), product-deq(A;B;a;b), IdLnk, sum-deq(A;B;a;b), sumdeq(a;b), union-deq(A;B;a;b), KindDeq, eqof(d), p  q, reduce(f;k;as), deq-member(eq;x;L), if b t else f fi, Y, 1of(t), P & Q, P  Q, Dec(P), null(as), P  Q, x:A. B(x), last(L), True, T

Lemmas

assert of band, and functionality wrt iff, squash wf, true wf, bnot thru band, assert of bor, or functionality wrt iff, band wf, bor wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, deq-member wf, bnot wf, not wf, Kind-deq wf, member append, l member wf, iseg weakening, iseg append0, cons one one, ecl-trans-state-append, ecl-trans-state-from wf, append assoc, append-cancellation-right, append-cancellation, last wf, length wf1, iseg append, last lemma, iseg antisymmetry, combine-ecl-trans-state0, append nil sq, top wf, decidable assert, null wf, append is nil, Id wf, fpf wf, Knd wf, ecl-trans-tuple wf, nat wf, bool wf, last induction, append wf, iff wf, iseg wf, assert wf, ecl-trans-h wf, ecl-trans-type wf, combine-ecl-tuples wf, le wf, event-info wf, ecl-trans-state wf, subtype rel self